($\lambda$$T$,$l_{1}$,$l_{2}$,$z$. $l_{1}$ $\leq$ $l_{2}$) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$($T$ List)$\rightarrow\downarrow$True$\rightarrow$Prop